es:ES, P:(E), j:E. (e:E. (e < j)  Dec(P(e)))  Dec(k:E. (k < j)  P(k)) 

latex

Definitions	{T}, A, P  Q, Dec(P), x(s), x:A. B(x), P  Q, t  T, , False, P & Q, P  Q, A c B
Lemmas	es-pred-causl, not wf, es-causl-iff, es-sender-causl, es-isrcv wf, es-first wf, decidable assert, event system wf, es-causle weakening, es-causl transitivity2, decidable wf, es-causl wf, es-E wf